Schreiber Topological Quantum Programming in TED-K

Accepted contribution to PlanQC 2022 (for further details see below):

---

• Hisham Sati and Urs Schreiber $\;$ (CQTS):

  
  

  Topological Quantum Programming in TED-K

  
  

  PlanQC 2022 33,

  (15 Sep 2022)

  
  

  download:

  • talk slides: pdf (view full screen)

  • video presentation: YT

  • extended abstract: arXiv:2209.08331, pdf

  • details: below

---

on a scheme for topological quantum programming in terms of twisted equivariant differential K-theory implemented in cohesive homotopy type theory (compatible with the quantum programming scheme QS).

Abstract. While the realization of scalable quantum computation will arguably require topological stabilization and, with it, topological-hardware-aware quantum programming and topological-quantum circuit verification, the proper combination of these strategies into dedicated topological quantum programming languages has not yet received attention.

Here we describe a fundamental and natural scheme for typed functional (hence verifiable) topological quantum programming which is fully topological-hardware aware – in that it natively reflects the universal fine technical detail of topological q-bits, namely of symmetry-protected (or enhanced) topologically ordered Laughlin-type anyon ground states in topological phases of quantum materials.

What makes this work is:

1. our recent result $[$SS22-Any, SS22-Ord$]$ that wavefunctions of realistic and technologically viable anyon species – namely of $\mathfrak{su}(2)$-anyons such as the popular Majorana/Ising anyons but also of computationally universal Fibonacci anyons – are reflected in the twisted equivariant differential (TED) K-cohomology of configuration spaces of codimension=2 nodal defects in the host material’s crystallographic orbifold;

2. combined with our earlier observation $[$SS20-EPB, SS20-Orb, Sc14$]$ that such TED generalized cohomology theories on orbifolds interpret intuitionistically-dependent linear data types in cohesive homotopy type theory (HoTT), supporting a powerful modern form of modal quantum logic.

Not only should this emulation of anyonic topological hardware functionality via TED-K implemented in cohesive HoTT make advanced formal software verification tools available for hardware-aware topological quantum programming, but the constructive nature of type checking a TED-K quantum program in cohesive HoTT on a classical computer using existing software (such as Agda-$\flat$), should amount at once to classically simulating the intended quantum computation at the deep level of physical topological q-bits.

This would make TED-K in cohesive HoTT an ideal software laboratory for topological quantum computation on technologically viable types of topological q-bits, complete with ready compilation to topological quantum circuits as soon as the hardware becomes available.

In this short note we give an exposition of the basic ideas, a quick review of the underlying results and a brief indication of the basic language constructs for anyon braiding via TED-K in cohesive HoTT. The language system is under development at the Center for Quantum and Topological Systems at the Research Institute of NYU Abu Dhabi.

Futher details:

The above file is just a brief announcement note. Here are some further details:

• (1) on the conceptual role of “topological hardware-awareness”

• (2) technical details of syntax/semantics for topological braid quantum gates

• On topological-hardware awareness via TED-K

  
  

  From a broad perspective, all quantum gates are linear maps/linear operators (semantically), hence are functions between linear types (syntactically). On a finer level however, some such (families of) linear operators/functions are much more readily implemented on given physical hardware than others.

  
  

  Existing quantum programming languages (QPLs) tend to have little reflection of this more detailed information, they are not “hardware aware”. In contrast, within TED-K implemented in cohesive HOTT one would have dependent linear types much as, say, Quipper does, but in addition infrastructure for naturally speaking about that particular class of quantum gates which matches expected TQC hardware functionality.

  
  

  Concretely, the elementary quantum gates that are expected to be realized by a topological quantum computer are of a very specific and peculiar kind: They are families of linear maps which are parameterized by elements of a braid group and which constitute a specific class of braid representations, namely “monodromy braid representations on $\mathfrak{su}(2)$-conformal blocks”.

  
  

  A traditional QPL like Quipper has no information about this. If one were to run (in the future) a Quipper program on a topological quantum computer, there would have to be a compiler involved which provides this missing information: The compiler would have to read in functions between linear types specified in Quipper, and would try to approximate them as composites of linear operators appearing in a monodromy braid representations on $\mathfrak{su}(2)$-conformal blocks.

  
  

  As a result, the generic Quipper program would tend to have an inefficient compilation to any given TQC machine. It would not be “aware” that this is the hardware that it is running on.

  
  

  In contrast, the TED-K language scheme that we are describing would be adding to the expressiveness of a language like Quipper the information about the native quantum gates that the TQC hardware would offer. The programmer would be provided with one very particular dependent linear homotopy type (the fiberwise TED-K type of fibrations of shapes of configuration spaces) and would be guaranteed that the linear maps (functions between linear types) which are obtained by type transport in/on this specific dependent linear type are those which the TQC hardware has an efficient implementation of.

  
  

  Of course, one could imagine adding this hardware-information by brute force to a traditional QPL: One could write, say, a Quipper library which encodes by hand the tensor functions which arise in $\mathfrak{su}(2)$-monodromy braid representations. The programmer could then decide to prefer composites of these pre-defined linear maps to build their quantum circuits, much like a contemporary high-level language programmer might choose to insert fine-tuned “assembler” commands for guarantee of verbatim efficient implementation on the underlying hardware.

  
  

  However, in both cases this would be a hack: the assembler code is alien to the ambient high-level language that calls it, just as Quipper would not provide any language handle on what it is that a would-be TQC library is providing.

  
  

  Our observation is that in homotopy type theory supporting a minimum of cohesion, this “TQC assembler code library”, if you wish, would automatically and natively be available, constructed “simply” as the 0-truncation of a certain dependent function type whose semantics is that of certain TED K-theory groups.

  
  

  This seems like a remarkable confluence of language and quantum physics for TQC. In the companion note Anyonic topological order in TED-K we explain that these TED-K types are a remarkably accurate reflection not just of topological quantum gates as such, but generally of the “topological phases of quantum materials” which are expected to serve as hardware implementing such gates. With a language for TED-K in cohesive HoTT, the distinction between a quantum programming language and an actual simulation of the underlying topological quantum hardware, at just the right “universal” level of anyon braiding, would disappear.

• Gauss-Manin- and Knizhnik-Zamolodchikov connections via abstract homotopy theory

  
  

  15 pages

  download:

  • pdf

  
  

  on formalizing Gauss-Manin connections (over fiber bundles) and hence the Knizhnik-Zamolodchikov connection (characterizing monodromy braid representations) in terms of abstract homotopy theory amenable to formalization in homotopy type theory.

Background results:

• Anyonic topological order in TED K-theory

• Anyonic defect branes in TED-K-theory

• Topological Quantum Gates in Homotopy Type Theory

• Quantum Certification via Linear Homotopy Types

Related articles:

• The Quantum Monadology

• Entanglement of Sections

• Quantum and Reality

Related presentations:

• Knots for quantum computation from defect branes

• TED K-theory of Cohomotopy moduli spaces and Anyonic Topological Order

• Topological Quantum Programming via Linear Homotopy Types,

  talk at Quantum Physics and Logic 2024, Buenes Aires, 15-19 July 2024

• Towards Certified Topological Quantum Programming via Linear Homotopy Types,

  talk at Quantum Information and Quantum Matter 2024,

  NYU Abu Dhabi, 27-31 May 2024

• Towards Quantum Programming via Linear Homotopy Types,

  talk at Homotopy Type Theory and Computing – Classical and Quantum,

  CQTS @ New York University Abu Dhabi, 19-21 April 2024

• Topological Quantum Programming via Linear Homotopy Types

  talk at: Homotopy Type Theory Electronic Seminar (01 Feb 2024)

  [video:YT, script:web]

• Effective Quantum Certification via Linear Homotopy Types,

  talk at Colloquium of the Topos Institute

  Part I: 13 April 2023 [video: YT, slides:pdf]

  Part II: 24 Aug 2023 [video:YT, slides:pdf]

• Towards verified topological hardware-aware quantum programming

  talk at CQTS & TII Workshop 2023, CQTS @ NYU Abu Dhabi, 24 Feb 2023

  [slides:pdf]

• Topological Quantum Programming in TED-K

  talk at PlanQC 2022 33 (15 Sep 2022)

  [slides:pdf, video: YT]

• Quantum Data Types via Linear Homotopy Type Theory

  talk at Workshop on Quantum Software @ QTML 2022, Naples, 12 Nov 2022

  [slides: pdf]

---